This will work in simulation. Will synthesis produce the expected results?

it should yes - but we should try with some real co-processor

I am not worried about the case when there is a module connected to the XIF and the parameter XInterface is set to 1. That will work as expected in both simulation and synthesis. What is less clear is what will be produced in synthesis when XInterface is 0.

In that case, coproc_done will always be 1 as its default value is set here

and it could go to zero only if this statement is true.
This can never be as the XInterface parameter would be 0 at design time - so the synthesizer would simply remove this logic, and there should not be any latch inferred.

Similarly, as this if statement would always be 0 , the coproc_done value here would never be assigned, so it would keep its default value at 1 - if you prefer for readability, I can do else coproc_done = 1'b1 - that's why when XInterface is 0 the CPU is Sequentially Equivalent.

If instead you refer to the situation that there is an illegal instruction and you are in the MULTI_CYCLE state, then no worries, you can never be here as you would never been entered this state if illegals and XInterace is 0. That's why when XInterface is 0 the CPU is Sequentially Equivalent.